$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{B}$), ${\it as}$:($T$ List), $d$:Top.
\\[0ex]($\exists$$a$:$T$. (($a$ $\in$ ${\it as}$) \& ($\uparrow$$P$($a$))))
\\[0ex]$\Rightarrow$ ((first $a$ $\in$ ${\it as}$ s.t. $P$($a$) else $d$) = hd(filter($\lambda$$a$.$P$($a$);${\it as}$)) $\in$ $T$)